D:Dsys, i:Id, s1, s2:M(i).state, k1, k2:Knd, v1:d-decl(D;i)(k1), v2:d-decl(D;i)(k2),
m1:{m:M(i).Msg| source(mlnk(m)) = i } List.
Feasible(D)
 <s1,doact(k1;v1),m1> = next-world-state(D;i;s2;k2;v2)  d-world-state(D;i)
 {s1 = (x.M(i).ef(k2,x,s2,v2)?s2(x))
 {& k1 = k2
 {& v1 = v2  d-decl(D;i)(k2)
 {& m1 = filter(m.source(mlnk(m)) = i;M(i).sends(k2,s2,v2))} 

latex

Definitions	t  T, {T}, mlnk(m), Msg(da), Msg(M), P & Q, Prop, next-world-state(D;i;s;k;v), x:A. B(x), P  Q, doact(k;v), M.Msg, Action(dec), d-world-state(D;i), 2of(t), 1of(t), x. t(x)
Lemmas	unit wf, inr equal, action wf, pi1 wf, pi2 wf, doact wf, next-world-state wf, d-world-state wf, d-feasible wf, lsrc wf, Id wf, d-m wf, ma-msg wf, d-decl wf, Knd wf, ma-st wf, dsys wf